Runtime Complexity (innermost) proof of /tmp/tmp77ZP9N/dyade.raml.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

0 CpxRelTRS

↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxWeightedTrs

↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 10 ms)

↳4 CpxWeightedTrs

↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CpxTypedWeightedTrs

↳7 CompletionProof (UPPER BOUND(ID), 0 ms)

↳8 CpxTypedWeightedCompleteTrs

↳9 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CpxTypedWeightedCompleteTrs

↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)

↳12 CpxRNTS

↳13 InliningProof (UPPER BOUND(ID), 1120 ms)

↳14 CpxRNTS

↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 19 ms)

↳16 CpxRNTS

↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 CpxRNTS

↳19 IntTrsBoundProof (UPPER BOUND(ID), 262 ms)

↳20 CpxRNTS

↳21 IntTrsBoundProof (UPPER BOUND(ID), 31 ms)

↳22 CpxRNTS

↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳24 CpxRNTS

↳25 IntTrsBoundProof (UPPER BOUND(ID), 325 ms)

↳26 CpxRNTS

↳27 IntTrsBoundProof (UPPER BOUND(ID), 7 ms)

↳28 CpxRNTS

↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳30 CpxRNTS

↳31 IntTrsBoundProof (UPPER BOUND(ID), 2813 ms)

↳32 CpxRNTS

↳33 IntTrsBoundProof (UPPER BOUND(ID), 421 ms)

↳34 CpxRNTS

↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳36 CpxRNTS

↳37 IntTrsBoundProof (UPPER BOUND(ID), 733 ms)

↳38 CpxRNTS

↳39 IntTrsBoundProof (UPPER BOUND(ID), 68 ms)

↳40 CpxRNTS

↳41 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳42 CpxRNTS

↳43 IntTrsBoundProof (UPPER BOUND(ID), 1321 ms)

↳44 CpxRNTS

↳45 IntTrsBoundProof (UPPER BOUND(ID), 92 ms)

↳46 CpxRNTS

↳47 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳48 CpxRNTS

↳49 IntTrsBoundProof (UPPER BOUND(ID), 831 ms)

↳50 CpxRNTS

↳51 IntTrsBoundProof (UPPER BOUND(ID), 56 ms)

↳52 CpxRNTS

↳53 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳54 CpxRNTS

↳55 IntTrsBoundProof (UPPER BOUND(ID), 1870 ms)

↳56 CpxRNTS

↳57 IntTrsBoundProof (UPPER BOUND(ID), 111 ms)

↳58 CpxRNTS

↳59 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳60 CpxRNTS

↳61 IntTrsBoundProof (UPPER BOUND(ID), 2077 ms)

↳62 CpxRNTS

↳63 IntTrsBoundProof (UPPER BOUND(ID), 133 ms)

↳64 CpxRNTS

↳65 FinalProof (⇔, 0 ms)

↳66 BOUNDS(1, n^2)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

The (relative) TRS S consists of the following rules:

Rewrite Strategy: INNERMOST

(1) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed relative TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

Rewrite Strategy: INNERMOST

(3) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined symbols to avoid conflicts with arithmetic symbols:

* => times

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

The TRS has the following type information:

times :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#mult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
dyade :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
dyade#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
:: :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
mult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
nil :: :::nil:#0:#s:#neg:#pos
mult#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#add :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#0 :: :::nil:#0:#s:#neg:#pos
#neg :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#s :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#pred :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#pos :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#succ :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos
#natmult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

Due to the following rules being added:

And the following fresh constants:

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

The TRS has the following type information:

times :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#mult :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
dyade :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
dyade#1 :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
:: :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
mult :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
nil :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
mult#1 :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#add :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#0 :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#neg :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#s :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#pred :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#pos :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#succ :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
#natmult :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ → :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
null_#add :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
null_#mult :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
null_#natmult :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
null_#pred :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ
null_#succ :: :::nil:#0:#s:#neg:#pos:null_#add:null_#mult:null_#natmult:null_#pred:null_#succ

Rewrite Strategy: INNERMOST

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

(12) Obligation:

Complexity RNTS consisting of the following rules:

(13) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

(14) Obligation:

Complexity RNTS consisting of the following rules:

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(16) Obligation:

Complexity RNTS consisting of the following rules:

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ #pred }
{ #succ }
{ #add }
{ #natmult }
{ #mult }
{ times }
{ mult#1, mult }
{ dyade, dyade#1 }

(18) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#pred}, {#succ}, {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: #pred
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + z

(20) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#pred}, {#succ}, {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: ?, size: O(n¹) [2 + z]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #pred
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(22) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#succ}, {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(24) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#succ}, {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: #succ
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + z

(26) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#succ}, {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: ?, size: O(n¹) [2 + z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #succ
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(28) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(30) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: #add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z + z'

(32) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#add}, {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]
#add: runtime: ?, size: O(n¹) [2·z + z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #add
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(34) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]
#add: runtime: O(1) [0], size: O(n¹) [2·z + z']

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(36) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]
#add: runtime: O(1) [0], size: O(n¹) [2·z + z']

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using PUBS for: #natmult
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 2 + 4·z + 4·z·z' + 2·z'

(38) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#natmult}, {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]
#add: runtime: O(1) [0], size: O(n¹) [2·z + z']
#natmult: runtime: ?, size: O(n²) [2 + 4·z + 4·z·z' + 2·z']

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #natmult
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(40) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(41) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(42) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: #mult
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 4·z·z' + 2·z'

(44) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#mult}, {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #mult
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(46) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(48) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: times
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 4·z·z' + 2·z'

(50) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {times}, {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: times
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(52) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(53) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(54) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: mult#1
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

Computed SIZE bound using CoFloCo for: mult
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(56) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {mult#1,mult}, {dyade,dyade#1}
Previous analysis results are:

#pred: runtime: O(1) [0], size: O(n¹) [2 + z]
#succ: runtime: O(1) [0], size: O(n¹) [2 + z]
#add: runtime: O(1) [0], size: O(n¹) [2·z + z']
#natmult: runtime: O(1) [0], size: O(n²) [2 + 4·z + 4·z·z' + 2·z']
#mult: runtime: O(1) [0], size: O(n²) [1 + 4·z·z' + 2·z']
times: runtime: O(1) [1], size: O(n²) [1 + 4·z·z' + 2·z']
mult#1: runtime: ?, size: INF
mult: runtime: ?, size: INF

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: mult#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 5 + 3·z

Computed RUNTIME bound using CoFloCo for: mult
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 6 + 3·z'

(58) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {dyade,dyade#1}
Previous analysis results are:

(59) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(60) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {dyade,dyade#1}
Previous analysis results are:

(61) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dyade
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

Computed SIZE bound using CoFloCo for: dyade#1
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(62) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {dyade,dyade#1}
Previous analysis results are:

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: dyade
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 2 + 8·z + 3·z·z'

Computed RUNTIME bound using KoAT for: dyade#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 10 + 8·z + 3·z·z' + 3·z'

(64) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed:
Previous analysis results are:

(65) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

(1) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CompletionProof (UPPER BOUND(ID) transformation)

(8) Obligation:

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

(12) Obligation:

(13) InliningProof (UPPER BOUND(ID) transformation)

(14) Obligation:

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(20) Obligation:

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(22) Obligation:

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

(24) Obligation:

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(26) Obligation:

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(28) Obligation:

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

(30) Obligation:

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(32) Obligation:

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(34) Obligation:

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

(36) Obligation:

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(38) Obligation:

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(40) Obligation:

(41) ResultPropagationProof (UPPER BOUND(ID) transformation)

(42) Obligation:

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(44) Obligation:

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(46) Obligation:

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

(48) Obligation:

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(50) Obligation:

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(52) Obligation:

(53) ResultPropagationProof (UPPER BOUND(ID) transformation)

(54) Obligation:

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(56) Obligation:

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(58) Obligation:

(59) ResultPropagationProof (UPPER BOUND(ID) transformation)

(60) Obligation:

(61) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(62) Obligation:

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(64) Obligation:

(65) FinalProof (EQUIVALENT transformation)

(66) BOUNDS(1, n^2)